\section{Formulazione di propriet\`a tramite HML}

L'HML (Hennessy-Milner logic) viene utilizzata per fare model checking dei processi specificati tramite il linguaggio CCS. Qui viene utilizzata per verificare l'assenza di deadlock o livelock. Mentre per la verifica dei primi esiste l'apposito comando in CWB ( \emph{deadlocks( agent)} ), per individuare la presenza di livelock occorre utilizzare l' HML. \\
Un livelock \`e una sequenza infinita di azioni non osservabili \emph{tau}.\\
Lo si modella pertanto utilizzando un massimo punto fisso in quanto la propriet\`a \`e valida a meno che non venga disprovata con una computazione finita.
\begin{verbatim}
 prop Taus = max(X.<tau>X);
\end{verbatim}
Logicamente un deadlock \`e presente in caso di sincronizzazione con il Timer. Pensando ad una impementazione in un qualche linguaggio di programmazione, se impostiamo il sender con un tempo di
re-invio troppo piccolo, esso bloccher\`a il sistema rispedendo sempre lo stesso pacchetto. Analogo \`e il caso del receiver se lo programmiamo in modo da rispondere con degli ack in modo frenetico.\\
Le formule riportate di seguito verificano ed attestano la presenza di livelock in questi casi.

\subsection{Implementazione standard}
\begin{verbatim}
checkprop(ABPok,Taus);
 true
prop Pr0 = <tau><tau><tau><ack0>Taus;
 checkprop(ABPok,Pr0);
 true
\end{verbatim}

\subsection{Perdita di pacchetti}
\subsubsection{Perdita di pacchetti solo dal lato Sender}
\begin{verbatim}
checkprop(ABPCHLS,Taus);
 true
prop Pr1 = <tau><tau><ack0>Taus;
 checkprop(ABPCHLS,Pr1);
 true
prop Pr2 = <tau><tau><ack0><tau><tau><tau><tau><ack1>Taus;
 checkprop(ABPCHLS,Pr2);
 true
\end{verbatim}

\subsubsection{Perdita di pacchetti solo dal lato Receiver}
\begin{verbatim}
checkprop(ABPCHLR,Taus);
 true
prop Pr3 = <tau><zero>Taus;
 checkprop(ABPCHLR,Pr3);
 true
prop Pr4 = <tau><zero><tau><tau><tau><tau><one>Taus;
 checkprop(ABPCHLR,Pr4);
 true
\end{verbatim}

\subsubsection{Perdita di pacchetti da entrambi i lati}
\begin{verbatim}
prop Pr5 = <zero>Taus;
 checkprop(ABPCHL,Pr5);
 true
prop Pr6 = <zero><tau><tau><ack0>Taus;
 checkprop(ABPCHL,Pr6);
 true
prop Pr7 = <zero><tau><tau><ack0><tau><tau><one>Taus;
 checkprop(ABPCHL,Pr7);
 true
prop Pr8 = <zero><tau><tau><ack0><tau><tau><one><tau><tau><ack1>Taus;
 checkprop(ABPCHL,Pr8);
 true
\end{verbatim}

\subsection{Perdita e duplicazione di pacchetti} 
Le formule utilizzate in caso di perdita di pacchetti si utilizzano anche nel caso di perdita e replicazione in quanto coprono le stesse casistiche, Si riportano pertanto solo i test e gli esiti prodotti.
\subsubsection{Perdita e duplicazione solo dal lato Sender}
\begin{verbatim}
 checkprop(ABPCHDS,Taus);
 true
 checkprop(ABPCHDS,Pr1);
 true
 checkprop(ABPCHDS,Pr2);
 true
\end{verbatim}

\subsubsection{Perdita e duplicazione solo dal lato Receiver}
\begin{verbatim}
 checkprop(ABPCHDR,Taus);
 true
 checkprop(ABPCHDR,Pr3);
 true
 checkprop(ABPCHDR,Pr4);
 true
\end{verbatim}

\subsubsection{Perdita e duplicazione da entrambi i lati}
\begin{verbatim}
 checkprop(ABPCHD,Pr5);
 true
 checkprop(ABPCHD,Pr6);
 true
 checkprop(ABPCHD,Pr7);
 true
 checkprop(ABPCHD,Pr8);
 true

\end{verbatim}

\subsection{Controllo dei deadlock}
Si riporta ora il codice immesso per controllare la presenza di deadlock nelle diverse implementazioni.
\begin{alltt}
\input{../ABP3.2.txt}
\end{alltt}


\chapter{Conclusioni}

Il protocollo soddisfa le propriet\`a richieste, ogni implementazione \`e priva di deadlock e presenta degli ovvi livelock che sono inevitabili. L'evoluzione pi\`u naturale di questo protocollo \`e lo \emph{sliding window} che, per\`o risulta ben pi\`u complesso da implementare. Si potrebbe anche pensare ad una implementazione in TCCS, dotando ogni azione di un delay $\epsilon$ per evitare dei livelock.\\
In principio avevo pensato di far emettere una azione visibile \emph{zero, one, ack0, ack1} anche in caso di ritrasmissione del pacchetto ma non sono riuscito a modellare il protocollo in modo da far rispettare la sequenza zero,ack0,one,ack1. Risultava infatti possibile una sequenza zero,ack0,zero a causa del diverso ordine di sincronizzazioni tra processi.\\
Il CWB si \`e rivelato un ottimo strumento, non comprendo per\`o una cosa.\\
Avevo definito un agente con una azione e sucessivamente, tale azione era ristretta. In pratica, diveniva una azione $\tau$. Quando \`e stato ora di verificare le propriet\`a, per\`o, accadeva un fatto strano. In presenza di tale azione, e della sua restrizione, il controllo della propriet\`a \emph{Taus} (si veda la sezione precedente) ritornava false. Togliendo l'azione incriminata la propriet\`a risultava essere true.\\ 
Questa cosa \`e alquanto assurda ma, come sempre in questi casi, temo di essermi perso qualcosa io, perch\`e il tool sembra non avere problemi.
